x1:Realizer. (Rframe?(x1))  (Rframe-loc(x1)  Id) 

latex

Definitions	if b then t else f fi , tt, ff, Rframe-loc(x1), t  T, Rframe?(x1), b, P  Q, x:A. B(x), False, Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, , Rnone(),
Lemmas	Rframe? wf, assert wf, true wf, false wf, es realizer wf